/****************************************************************************
 * Elisa 1.0                                                                *
 *--------------------------------------------------------------------------*
 * Author: Laurent Granvilliers                                             *
 * Copyright (c) 2004 Laboratoire d'Informatique de Nantes Atlantique       *
 *--------------------------------------------------------------------------*
 * Elisa is distributed WITHOUT ANY WARRANTY. Read the associated           *
 * COPYRIGHT file for more details.                                         *
 *--------------------------------------------------------------------------*
 * elisa_real_constraint.h                                                  *
 ****************************************************************************/

/**
 * @file elisa_real_constraint.h
 * @brief Classes for interval constraints.
 */


#ifndef _ELISA_REAL_CONSTRAINT_H
#define _ELISA_REAL_CONSTRAINT_H

#include <iostream>
#include <set>
#include <vector>
#include "elisa_defs.h"
#include "elisa_constraint.h"
#include "elisa_real_expr.h"


NAMESPACE_ELISA


//---------------------
// Forward declarations
//---------------------
class RealConstraint;
class RealConstraintVisitor;
class RealConstraintRep;
class RealConstraintRepEq;
class RealConstraintRepInf;
class RealConstraintRepSup;
//---------------------


/**
 * @ingroup Interval
 * @class RealConstraintRep
 * @brief Tree-representation of real constraints
 */
class RealConstraintRep : public ConstraintRep
{
public:
	/**
 	 * Constructor
 	 * @param rel the relation
 	 * @param prefix true if this is prefixed
 	 */
	RealConstraintRep (const std::string & rel,
	                   bool prefix);

	/**
 	 * Copy Constructor
 	 */
	RealConstraintRep (const RealConstraintRep & c);

	/**
 	 * Destructor
 	 */
	virtual
	~RealConstraintRep();

	/**
 	 * Return a copy of *this
 	 */
	virtual RealConstraintRep *copy() const = 0;

	/**
 	 * Visitor
 	 */
	virtual void visit(RealConstraintVisitor & v) = 0;

	/**
 	 * Print the constraint
 	 * @param os the stream where the constraint must be printed
 	 */
	void print(std::ostream & os) const;

	/**
 	 * Return a new expression corresponding to the functional expression
 	 * of the constraint
 	 */
	virtual RealExpr *function() const = 0;

protected:
	// @var relation symbol
	std::string _rel;
	// @var true for prefix relations
	bool _prefix;
};



/**
 * @ingroup Interval
 * @class RealConstraintVisitor
 * @brief Visitor of real constraints
 */
class RealConstraintVisitor
{
public:
	/**
 	 * Default Constructor
 	 */
	RealConstraintVisitor ();

	/**
 	 * Destructor
 	 */
	virtual ~RealConstraintVisitor ();

	/// @name Visit of each constraint type
	//@{
	/// Sends the visitor to the constraint
	virtual void visit(RealConstraintRep & c) = 0;

	/// Call of the visitor from an equality constraint
	virtual void visited(RealConstraintRepEq & c) = 0;

	/// Call of the visitor from an inequality constraint <=
	virtual void visited(RealConstraintRepInf & c) = 0;

	/// Call of the visitor from an inequality constraint >=
	virtual void visited(RealConstraintRepSup & c) = 0;
	//@}
};



/**
 * @ingroup Constraint
 * @class RealConstraintBinaryRep
 * @brief Tree-representation of binary real constraints
 */
class RealConstraintBinaryRep : public RealConstraintRep
{
public:
	/**
 	 * Constructor
 	 * @param l left  expression of the constraint
 	 * @param r right expression of the constraint
 	 * @param rel string that contains the relation for printing
 	 */
	RealConstraintBinaryRep (RealExpr *l,
	                         RealExpr *r,
	                         const std::string & rel);

	/**
 	 * Destructor
 	 */
	virtual
	~RealConstraintBinaryRep ();

	/**
 	 * @brief Access to the left expression
 	 * @return a pointer to the left expression
 	 */
	RealExpr *left();

	/**
 	 * @brief Access to the left expression
 	 * @return a pointer to the left expression
 	 */
	RealExpr *const_left() const;

	/**
 	 * @brief Access to the right expression
 	 * @return a pointer to the right expression
 	 */
	RealExpr *right();

	/**
 	 * @brief Access to the right expression
 	 * @return a pointer to the right expression
 	 */
	RealExpr *const_right() const;
};



/**
 * @ingroup Constraint
 * @class RealConstraintRepEq
 * @brief Tree-representation of real equations
 */
class RealConstraintRepEq : public RealConstraintBinaryRep
{
public:
	/**
 	 * Constructor
 	 * @param l left real expression
 	 * @param r right real expression
 	 */
	RealConstraintRepEq (RealExpr *l,
	                     RealExpr *r);

	/**
 	 * Copy constructor
 	 * @param c the equation to copy
 	 */
	RealConstraintRepEq (const RealConstraintRepEq & c);


	/**
 	 * Destructor
 	 */
	~RealConstraintRepEq ();

	/// @name Methods from base class
	//@{
	void visit(RealConstraintVisitor & v);

	RealConstraintRep *copy() const;

	RealExpr *function() const;
	//@}

private:
	// Copy protection
	RealConstraintRepEq &
	operator=(const RealConstraintRepEq & c);
};


/**
 * @ingroup Constraint
 * @class RealConstraintRepInf
 * @brief Tree-representation of real inequality constraints <=
 */
class RealConstraintRepInf : public RealConstraintBinaryRep
{
public:
	/**
 	 * Constructor
 	 * @param l left real expression
 	 * @param r right real expression
 	 */
	RealConstraintRepInf (RealExpr *l,
	                      RealExpr *r);

	/**
 	 * Copy constructor
 	 * @param c the equation to copy
 	 */
	RealConstraintRepInf (const RealConstraintRepInf & c);

	/**
 	 * Destructor
 	 */
	~RealConstraintRepInf ();

	/// @name Methods from base class
	//@{
	void visit(RealConstraintVisitor & v);

	RealConstraintRep *copy() const;

	RealExpr *function() const;
	//@}

private:
	// Copy protection
	RealConstraintRepInf &
	operator=(const RealConstraintRepInf & c);
};


/**
 * @ingroup Constraint
 * @class RealConstraintRepSup
 * @brief Tree-representation of real inequality constraints >=
 */
class RealConstraintRepSup : public RealConstraintBinaryRep {
public:
	/**
 	 * Constructor
 	 * @param l left real expression
 	 * @param r right real expression
 	 */
	RealConstraintRepSup (RealExpr *l,
	                      RealExpr *r);

	/**
 	 * Copy constructor
 	 * @param c the equation to copy
 	 */
	RealConstraintRepSup (const RealConstraintRepSup & c);

	/**
 	 * Destructor
 	 */
	~RealConstraintRepSup ();

	/// @name Methods from base class
	//@{
	void visit(RealConstraintVisitor & v);

	RealConstraintRep *copy() const;

	RealExpr *function() const;
	//@}

private:
	/// Copy protection
	RealConstraintRepSup &
	operator=(const RealConstraintRepSup & c);
};



/**
 * @ingroup Constraint
 * @class RealConstraint
 * @brief Real constraint (==, >=, <=)
 */
class RealConstraint : public Constraint 
{
public:
	/**
 	 * Default constructor
 	 */
	RealConstraint();

	/**
 	 * @brief Constructor
 	 * build a new RealConstraint given a tree representation of a Real constraint
 	 * @param c the RealConstraintRep
 	 */
	RealConstraint(RealConstraintRep & c);

	/**
 	 * @brief Constructor
 	 * build a new RealConstraint given a tree representation of a Real constraint
 	 * @param c the RealConstraintRep
 	 */
	RealConstraint(RealConstraintRep *c);

	/**
 	 * Copy constructor
 	 */
	RealConstraint(const RealConstraint & c);

	/**
 	 * Destructor
 	 */
	~RealConstraint();

	/**
 	 * Copy operator
 	 */
	RealConstraint & operator=(const RealConstraint & c);

	/**
 	 * Copy the tree representation of the constraint
 	 * @return a copy of the tree-representation of the constraint
 	 */
	RealConstraintRep *copyRep() const;

	/**
 	 * @brief pointer to the tree representation o the constraint
 	 * @return the tree-representation of the constraint
 	 */
	RealConstraintRep *rep();

	/**
 	 * @brief pointer to the tree representation o the constraint
 	 * @return the tree-representation of the constraint
 	 */
	const RealConstraintRep *const_rep() const;

	/**
 	 * Given a constraint f rel g, returns a new expression f - g
 	 */
	RealExpr *function() const;

	/**
 	 * Give the type of the model
 	 * @return a string that contains the name of the type
 	 */
	std::string type() const
	{
		return "RealConstraint";
	}
};

END_NAMESPACE_ELISA


//------------------------------------------------------------------------
// Operators
//------------------------------------------------------------------------

/**
 * @relates RealConstraint
 * @brief Creation of constraint l==r
 */
elisa::RealConstraint
operator==(const elisa::RealExpr & l,
           const elisa::RealExpr & r);


/**
 * @relates RealConstraint
 * @brief Creation of constraint l<=r
 */
elisa::RealConstraint
operator<=(const elisa::RealExpr & l,
           const elisa::RealExpr & r);


/**
 * @relates RealConstraint
 * @brief Creation of constraint l>=r
 */
elisa::RealConstraint
operator>=(const elisa::RealExpr & l,
           const elisa::RealExpr & r);

#endif // ELISA_REAL_CONSTRAINT
